00100 ∀(X1 X2)(P(X1 X2) ∧P(X2 X3) ⊃ G(X1 X3)); 00200 ; 00300 ∀(X2)∃(X1)P(X1 X2); 00400 ; 00500 ∃(X1 X2)G(X1 X2); 00600 ;